(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(assert (let ((?v_96 (<= x_50 x_0)) (?v_97 (<= x_51 x_0)) (?v_77 (= x_55 x_20)) (?v_76 (= x_47 x_26)) (?v_75 (= x_49 x_24)) (?v_68 (= x_48 x_23)) (?v_67 (= x_46 x_25)) (?v_69 (= x_56 x_19)) (?v_57 (+ x_10 1))) (let ((?v_66 (= x_37 ?v_57)) (?v_59 (= x_10 x_9)) (?v_63 (= x_10 x_32)) (?v_71 (= x_36 x_16)) (?v_74 (= x_38 x_13)) (?v_58 (+ x_13 1))) (let ((?v_84 (= x_38 ?v_58)) (?v_72 (= x_58 x_22)) (?v_73 (= x_51 x_12)) (?v_79 (= x_13 x_12)) (?v_82 (= x_13 x_33)) (?v_86 (= x_35 x_14)) (?v_65 (= x_57 x_21)) (?v_62 (= x_50 x_9)) (?v_87 (= x_37 x_10)) (?v_3 (= x_9 x_0)) (?v_2 (+ (+ x_0 x_4) x_1))) (let ((?v_16 (= x_9 ?v_2)) (?v_4 (= x_12 x_0)) (?v_20 (= x_12 ?v_2)) (?v_9 (not ?v_3))) (let ((?v_12 (not ?v_4)) (?v_15 (<= x_10 x_0)) (?v_19 (<= x_13 x_0)) (?v_29 (not ?v_16))) (let ((?v_23 (and ?v_15 ?v_29)) (?v_30 (not ?v_20))) (let ((?v_26 (and ?v_19 ?v_30)) (?v_104 (= x_50 x_54))) (let ((?v_102 (not ?v_104)) (?v_101 (+ (+ x_54 x_4) x_1))) (let ((?v_115 (= x_50 ?v_101)) (?v_107 (= x_51 x_54))) (let ((?v_103 (not ?v_107)) (?v_119 (= x_51 ?v_101)) (?v_114 (not (<= x_37 x_54))) (?v_118 (not (<= x_38 x_54)))) (let ((?v_122 (or ?v_114 ?v_115)) (?v_125 (or ?v_118 ?v_119)) (?v_36 (- x_37 x_2))) (let ((?v_88 (<= ?v_36 x_39)) (?v_89 (<= ?v_36 x_40)) (?v_37 (- x_38 x_2))) (let ((?v_90 (<= ?v_37 x_41)) (?v_91 (<= ?v_37 x_42)) (?v_38 (+ x_37 x_2))) (let ((?v_92 (<= x_39 ?v_38)) (?v_93 (<= x_40 ?v_38)) (?v_39 (+ x_38 x_2))) (let ((?v_94 (<= x_41 ?v_39)) (?v_95 (<= x_42 ?v_39)) (?v_70 (and (not ?v_59) (not ?v_63))) (?v_85 (and (not ?v_79) (not ?v_82))) (?v_0 (- x_0 x_5)) (?v_1 (- x_0 x_8)) (?v_5 (- x_14 x_15)) (?v_6 (- x_10 x_6)) (?v_7 (- x_16 x_17)) (?v_8 (- x_13 x_7)) (?v_10 (- x_14 x_19)) (?v_11 (- x_10 x_0)) (?v_13 (- x_16 x_20)) (?v_14 (- x_13 x_0)) (?v_24 (- x_19 x_15))) (let ((?v_17 (* ?v_24 1000)) (?v_18 (* (- x_19 x_17) 1000)) (?v_21 (* (- x_20 x_15) 1000)) (?v_27 (- x_20 x_17))) (let ((?v_22 (* ?v_27 1000)) (?v_25 (- x_0 x_6)) (?v_28 (- x_0 x_7)) (?v_64 (+ x_21 x_1)) (?v_83 (+ x_22 x_1)) (?v_31 (- x_25 x_19)) (?v_33 (- x_26 x_20)) (?v_41 (- x_35 x_46)) (?v_42 (- x_37 x_48)) (?v_43 (- x_36 x_47)) (?v_44 (- x_38 x_49)) (?v_45 (+ x_37 1)) (?v_46 (+ x_38 1)) (?v_48 (- x_10 x_2)) (?v_49 (- x_13 x_2)) (?v_50 (+ x_10 x_2)) (?v_51 (+ x_13 x_2)) (?v_53 (- x_14 x_25)) (?v_54 (- x_10 x_23)) (?v_55 (- x_16 x_26)) (?v_56 (- x_13 x_24)) (?v_60 (* x_57 2)) (?v_61 (+ x_27 x_29)) (?v_80 (* x_58 2)) (?v_81 (+ x_28 x_30)) (?v_98 (- x_54 x_5)) (?v_99 (- x_54 x_8)) (?v_100 (+ x_54 x_1)) (?v_105 (- x_35 x_44)) (?v_106 (- x_37 x_59)) (?v_108 (- x_36 x_45)) (?v_109 (- x_38 x_60)) (?v_110 (- x_35 x_56)) (?v_111 (- x_37 x_54)) (?v_112 (- x_36 x_55)) (?v_113 (- x_38 x_54)) (?v_123 (- x_56 x_44))) (let ((?v_116 (* ?v_123 1000)) (?v_117 (* (- x_56 x_45) 1000)) (?v_120 (* (- x_55 x_44) 1000)) (?v_126 (- x_55 x_45))) (let ((?v_121 (* ?v_126 1000)) (?v_124 (- x_54 x_59)) (?v_127 (- x_54 x_60)) (?v_128 (- x_46 x_56)) (?v_129 (- x_47 x_55)) (?v_32 (* (* x_1 999) (/ 1 1000))) (?v_34 (* (* x_1 1001) (/ 1 1000))) (?v_35 (+ x_34 (/ 1001 1000))) (?v_40 (+ x_43 (/ 1001 1000))) (?v_47 (+ x_18 (/ 1001 1000))) (?v_52 (+ x_31 (/ 1001 1000))) (?v_78 (+ x_18 (/ 999 1000)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_1 0)) (not (<= x_2 0))) (not (< x_3 (+ x_2 (* (* (+ (* (* x_1 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (not (<= x_4 0))) (< x_5 (- (* (* (- (- x_1 x_3) 1) 999) (/ 1 2)) 1))) (not (< x_5 (* (* (+ (+ (+ x_4 x_2) x_3) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_8 0))) (<= x_8 (- x_4 (+ (+ x_2 (* (* (+ x_1 2) 1001) (/ 1 999))) (/ 1 2))))) (<= ?v_0 x_6)) (<= ?v_0 x_7)) (<= x_6 ?v_1)) (<= x_7 ?v_1)) (<= (- x_6 x_6) x_3)) (<= (- x_7 x_6) x_3)) (<= (- x_6 x_7) x_3)) (<= (- x_7 x_7) x_3)) (or (and ?v_3 (<= x_10 x_11)) ?v_16)) (or (and ?v_4 (<= x_13 x_11)) ?v_20)) (or ?v_3 ?v_4)) (or ?v_9 (and (<= (* (* ?v_6 999) (/ 1 1000)) ?v_5) (<= ?v_5 (* (* ?v_6 1001) (/ 1 1000)))))) (or ?v_12 (and (<= (* (* ?v_8 999) (/ 1 1000)) ?v_7) (<= ?v_7 (* (* ?v_8 1001) (/ 1 1000)))))) (or (or ?v_9 ?v_15) (and (and (not (< x_18 x_19)) (<= (* (* ?v_11 999) (/ 1 1000)) ?v_10)) (<= ?v_10 (* (* ?v_11 1001) (/ 1 1000)))))) (or (or ?v_12 ?v_19) (and (and (not (< x_18 x_20)) (<= (* (* ?v_14 999) (/ 1 1000)) ?v_13)) (<= ?v_13 (* (* ?v_14 1001) (/ 1 1000)))))) (or ?v_23 (and (<= x_21 (+ (+ (* (* (+ (+ (+ x_6 (* ?v_17 (/ 1 999))) x_7) (* ?v_18 (/ 1 999))) 1) (/ 1 2)) x_2) (/ 3001 1998))) (not (< x_21 (- (- (* (* (+ (+ (+ x_6 (* ?v_17 (/ 1 1001))) x_7) (* ?v_18 (/ 1 1001))) 1) (/ 1 2)) x_2) (/ 1 2))))))) (or ?v_26 (and (<= x_22 (+ (+ (* (* (+ (+ (+ x_6 (* ?v_21 (/ 1 999))) x_7) (* ?v_22 (/ 1 999))) 1) (/ 1 2)) x_2) (/ 3001 1998))) (not (< x_22 (- (- (* (* (+ (+ (+ x_6 (* ?v_21 (/ 1 1001))) x_7) (* ?v_22 (/ 1 1001))) 1) (/ 1 2)) x_2) (/ 1 2))))))) (or ?v_23 (and (<= (* (* ?v_25 999) (/ 1 1000)) ?v_24) (<= ?v_24 (* (* ?v_25 1001) (/ 1 1000)))))) (or ?v_26 (and (<= (* (* ?v_28 999) (/ 1 1000)) ?v_27) (<= ?v_27 (* (* ?v_28 1001) (/ 1 1000)))))) (or ?v_29 (= x_23 ?v_64))) (or ?v_30 (= x_24 ?v_83))) (or ?v_29 (and (<= ?v_32 ?v_31) (<= ?v_31 ?v_34)))) (or ?v_30 (and (<= ?v_32 ?v_33) (<= ?v_33 ?v_34)))) (<= x_34 x_35)) (<= x_34 x_36)) (<= x_35 ?v_35)) (<= x_36 ?v_35)) ?v_88) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93) ?v_94) ?v_95) (<= x_43 x_34)) (<= x_43 x_44)) (<= x_43 x_45)) (<= x_44 ?v_40)) (<= x_45 ?v_40)) (<= x_46 x_34)) (<= x_47 x_34)) (<= (* (* ?v_42 999) (/ 1 1000)) ?v_41)) (<= (* (* ?v_44 999) (/ 1 1000)) ?v_43)) (<= ?v_41 (* (* ?v_42 1001) (/ 1 1000)))) (<= ?v_43 (* (* ?v_44 1001) (/ 1 1000)))) (or (or (not (<= x_37 x_50)) (not (< x_50 ?v_45))) (= x_37 x_50))) (or (or (not (<= x_38 x_51)) (not (< x_51 ?v_46))) (= x_38 x_51))) (or (or (not (<= x_37 x_52)) (not (< x_52 ?v_45))) (= x_37 x_52))) (or (or (not (<= x_38 x_53)) (not (< x_53 ?v_46))) (= x_38 x_53))) (<= x_18 x_14)) (<= x_18 x_16)) (<= x_14 ?v_47)) (<= x_16 ?v_47)) (<= ?v_48 x_27)) (<= ?v_48 x_28)) (<= ?v_49 x_29)) (<= ?v_49 x_30)) (<= x_27 ?v_50)) (<= x_28 ?v_50)) (<= x_29 ?v_51)) (<= x_30 ?v_51)) (<= x_31 x_18)) (<= x_31 x_15)) (<= x_31 x_17)) (<= x_15 ?v_52)) (<= x_17 ?v_52)) (<= x_25 x_18)) (<= x_26 x_18)) (<= (* (* ?v_54 999) (/ 1 1000)) ?v_53)) (<= (* (* ?v_56 999) (/ 1 1000)) ?v_55)) (<= ?v_53 (* (* ?v_54 1001) (/ 1 1000)))) (<= ?v_55 (* (* ?v_56 1001) (/ 1 1000)))) (or (or (not (<= x_10 x_9)) (not (< x_9 ?v_57))) ?v_59)) (or (or (not (<= x_13 x_12)) (not (< x_12 ?v_58))) ?v_79)) (or (or (not (<= x_10 x_32)) (not (< x_32 ?v_57))) ?v_63)) (or (or (not (<= x_13 x_33)) (not (< x_33 ?v_58))) ?v_82)) (= x_52 (+ x_50 x_1))) (= x_53 (+ x_51 x_1))) (= x_32 (+ x_9 x_1))) (= x_33 (+ x_12 x_1))) (= x_11 (+ x_0 x_1))) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (< x_18 x_14) (< x_18 x_16)) (< x_18 x_34)) (<= x_34 x_14)) (<= x_34 x_16)) (or (= x_34 x_14) (= x_34 x_16))) ?v_86) ?v_71) ?v_65) ?v_72) ?v_62) ?v_73) ?v_87) ?v_74) ?v_68) ?v_75) ?v_67) ?v_76) ?v_69) ?v_77) (= x_39 x_27)) (= x_41 x_29)) (= x_40 x_28)) (= x_42 x_30)) (and (and (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and (= x_18 x_14) (<= ?v_78 x_35)) (<= x_35 ?v_47)) (or (or (and (and (and (and ?v_59 (<= (- ?v_61 1) ?v_60)) (<= ?v_60 (+ ?v_61 1))) ?v_66) ?v_62) (and (and (and ?v_63 (= x_37 (+ ?v_64 1))) (= x_50 (+ (+ x_9 x_4) x_1))) ?v_65)) (and (and (and ?v_70 ?v_66) ?v_65) ?v_62))) (or (or (and (and (and ?v_59 (= x_56 x_18)) ?v_67) ?v_68) (and (and (and ?v_63 (= x_46 x_18)) (= x_48 (- x_37 1))) ?v_69)) (and (and (and ?v_70 ?v_69) ?v_67) ?v_68))) ?v_71) ?v_72) ?v_73) ?v_74) ?v_75) ?v_76) ?v_77) (and (and (and (and (and (and (and (and (and (and (and (= x_18 x_16) (<= ?v_78 x_36)) (<= x_36 ?v_47)) (or (or (and (and (and (and ?v_79 (<= (- ?v_81 1) ?v_80)) (<= ?v_80 (+ ?v_81 1))) ?v_84) ?v_73) (and (and (and ?v_82 (= x_38 (+ ?v_83 1))) (= x_51 (+ (+ x_12 x_4) x_1))) ?v_72)) (and (and (and ?v_85 ?v_84) ?v_72) ?v_73))) (or (or (and (and (and ?v_79 (= x_55 x_18)) ?v_76) ?v_75) (and (and (and ?v_82 (= x_47 x_18)) (= x_49 (- x_38 1))) ?v_77)) (and (and (and ?v_85 ?v_77) ?v_76) ?v_75))) ?v_86) ?v_65) ?v_62) ?v_87) ?v_68) ?v_67) ?v_69)) ?v_88) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93) ?v_94) ?v_95) (= x_34 x_18)))) (or (and (and (and (and (and (and (and (not ?v_96) (not ?v_97)) (= x_43 x_34)) (= x_59 x_37)) (= x_60 x_38)) (= x_44 x_35)) (= x_45 x_36)) (= x_54 ?v_2)) (and (and (and (and (and (and (or ?v_96 ?v_97) (= x_54 x_0)) (= x_43 x_31)) (= x_44 x_15)) (= x_45 x_17)) (= x_59 x_6)) (= x_60 x_7)))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (not (<= ?v_98 x_59)) (not (<= ?v_98 x_60))) (not (<= x_59 ?v_99))) (not (<= x_60 ?v_99))) (not (<= (- x_59 x_59) x_3))) (not (<= (- x_60 x_59) x_3))) (not (<= (- x_59 x_60) x_3))) (not (<= (- x_60 x_60) x_3))) (and (or ?v_102 (not (<= x_37 ?v_100))) (not ?v_115))) (and (or ?v_103 (not (<= x_38 ?v_100))) (not ?v_119))) (and ?v_102 ?v_103)) (and ?v_104 (or (not (<= (* (* ?v_106 999) (/ 1 1000)) ?v_105)) (not (<= ?v_105 (* (* ?v_106 1001) (/ 1 1000))))))) (and ?v_107 (or (not (<= (* (* ?v_109 999) (/ 1 1000)) ?v_108)) (not (<= ?v_108 (* (* ?v_109 1001) (/ 1 1000))))))) (and (and ?v_104 ?v_114) (or (or (< x_34 x_56) (not (<= (* (* ?v_111 999) (/ 1 1000)) ?v_110))) (not (<= ?v_110 (* (* ?v_111 1001) (/ 1 1000))))))) (and (and ?v_107 ?v_118) (or (or (< x_34 x_55) (not (<= (* (* ?v_113 999) (/ 1 1000)) ?v_112))) (not (<= ?v_112 (* (* ?v_113 1001) (/ 1 1000))))))) (and ?v_122 (or (not (<= x_57 (+ (+ (* (* (+ (+ (+ x_59 (* ?v_116 (/ 1 999))) x_60) (* ?v_117 (/ 1 999))) 1) (/ 1 2)) x_2) (/ 3001 1998)))) (< x_57 (- (- (* (* (+ (+ (+ x_59 (* ?v_116 (/ 1 1001))) x_60) (* ?v_117 (/ 1 1001))) 1) (/ 1 2)) x_2) (/ 1 2)))))) (and ?v_125 (or (not (<= x_58 (+ (+ (* (* (+ (+ (+ x_59 (* ?v_120 (/ 1 999))) x_60) (* ?v_121 (/ 1 999))) 1) (/ 1 2)) x_2) (/ 3001 1998)))) (< x_58 (- (- (* (* (+ (+ (+ x_59 (* ?v_120 (/ 1 1001))) x_60) (* ?v_121 (/ 1 1001))) 1) (/ 1 2)) x_2) (/ 1 2)))))) (and ?v_122 (or (not (<= (* (* ?v_124 999) (/ 1 1000)) ?v_123)) (not (<= ?v_123 (* (* ?v_124 1001) (/ 1 1000))))))) (and ?v_125 (or (not (<= (* (* ?v_127 999) (/ 1 1000)) ?v_126)) (not (<= ?v_126 (* (* ?v_127 1001) (/ 1 1000))))))) (and ?v_115 (not (= x_48 (+ x_57 x_1))))) (and ?v_119 (not (= x_49 (+ x_58 x_1))))) (and ?v_115 (or (not (<= ?v_32 ?v_128)) (not (<= ?v_128 ?v_34))))) (and ?v_119 (or (not (<= ?v_32 ?v_129)) (not (<= ?v_129 ?v_34))))))))))))))))))))))))))
(check-sat)
(exit)
